A:Type, B, C:(AType), eq:EqDecider(A), f:a:A fp B(a), g:a:A fp C(a).
(x:A. (x  dom(f))  (x  dom(g))  (B(x) r C(x)))  (f || g  ) 

latex

Definitions	x:A. B(x), x(s), P  Q, t  T, , f || g, P & Q, x. t(x)
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-ap wf, fpf wf, deq wf